ProveDetails Command

ProveDetails( <Boolean Expression> ): Returns some details of the result of the automated proof.

Normally, GeoGebra decides whether a boolean expression is true or not by using numerical computations. However, the ProveDetails command uses symbolic methods to determine whether a statement is true or false in general. This command works like the Prove command, but also returns some details of the result as a list:

An empty list {} if GeoGebra cannot determine the answer.
A list with one element: {false}, if the statement is not true in general.
A list with one element: {true}, if the statement is always true (in all cases when the diagram can be constructed).
A list with more elements, containing the boolean value true and another list for some so-called non-degeneracy conditions, if the statement is true under certain conditions, e.g. {true, {"AreCollinear(A,B,C),AreEqual(C,D)"}}. This means that if none of the conditions are true (and the diagram can be constructed), then the statement will be true.
A list {true,{"…"}}, if the statement is true under certain conditions, but these conditions cannot be translated to human readable form for some reasons.

Let us define a triangle with vertices A, B and C, and define D=MidPoint(B,C), E=MidPoint(A,C), p=Line(A,B), q=Line(D,E). Now ProveDetails(p∥q) returns {true}, which means that if the diagram can be constructed, then the midline DE of the triangle is parallel to the side AB.

Let AB be the segment a, and define C=MidPoint(A,B), b=PerpendicularBisector(A,B), D=Intersect(a,b). Now ProveDetails(C==D) returns {true,{"AreEqual(A,B)"}}: it means that if the points A and B differ, then the points C and D will coincide.

Let AB be the segment a, and define l=Line(A,B). Let C be an arbitrary point on line l, moreover let b=Segment(B,C), c=Segment(A,C). Now ProveDetails(a==b+c) returns {true,{"a+b==c", "b==a+c"}}: it means that if neither \(a+b=c\), nor \(b=a+c\), then \(a=b+c\).

It is possible that the list of the non-degeneracy conditions is not the simplest possible set. For the above example, the simplest set would be the empty set.